Nuprl Lemma : same-sender-index 0,22
es:ES, e, e':E.
isrcv(e)
 isrcv(e')
 (e = e'
 (
 (sender(e) = sender(e')  E & lnk(e) = lnk(e')  IdLnk & index(e) = index(e')  ) 
latex

Definitionst  T, P  Q, x:A. B(x), sender(e), lnk(e), sends(l;e), (Msg on l), ||as||, #$n, {i..j}, {x:A| B(x) }, x:AB(x), True, T, ES, E, isrcv(e), b, index(e), , s = t, Type, Prop, IdLnk, x:AB(x), P & Q, <a,b>, P  Q, P  Q, (e <loc e'), s ~ t, {T}, SQType(T), A/x,y. B(x;y), 1of(t), False, A, ij, left+right, P  Q, Id, loc(e), Void, a<b, Case b of inl(x)  s(x) ; inr(y)  t(y), if b t else f fi, destination(l), source(l),
Lemmases-axioms, lsrc wf, ldst wf, es-loc wf, true wf, es-loc-pred, implies functionality wrt iff, or functionality wrt iff, es-locl-iff, es-isrcv-loc, Id wf, es-locl-antireflexive, es-locl wf, IdLnk wf, es-index wf, squash wf, assert wf, es-isrcv wf, es-E wf, event system wf, int seg wf, length wf1, es-Msgl wf, es-sends wf, es-lnk wf, es-sender wf

origin